Inference at * 
Iof proof for Lemma adjacent-member:


  T:Type, L:(T List), x, y:T. adjacent(T;L;x;y)  {(x  L) & (y  L)} 

latex

 by ((Auto) 
CollapseTHEN (((((FLemma `adjacent-before` [-1]) 
THENM (((
THFLemma `l_before_member`[-1]) 
THENM (FLemma `l_before_member2`[-2]))))) 
TCollapseTHENA (Auto
TC)))) 

latex

TC1: 

TC1: 1. T : Type
TC1: 2. L : T List
TC1: 3. x : T
TC1: 4. y : T
TC1: 5. adjacent(T;L;x;y)
TC1: 6. x before y  L
TC1: 7. (y  L)
TC1: 8. (x  L)
TC1:   {(x  L) & (y  L)}
TC.

Definitions	adjacent(T;L;x;y), type List, P & Q, x:A  B(x), , Type, {T}, x before y  l, x:A. B(x), P  Q, x:AB(x), (x  l)
Lemmas	adjacent wf, l member wf, guard wf, adjacent-before, l before member, l before member2